package controller.preprocessor;

import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStreamReader;

import model.cnf.FileCNF;
import model.preprocessor.PreProcessorResult;
import model.preprocessor.PreProcessorResultStatus;

/**
 * This Class provide a model for you to add and implement your own preprocessor. 
 * It take care of the maximum of operation so that you only need the give the minimum amount of information and add as quickly as possible your preprocessor.
 * 
 * So to add your preprocessor you only need to implement the hasTimeout method, return false if your preprocessor has no timeout, getCommandLine that return the command line that should be run and also checkParameter that check if everything is fine with the parameter (I recommend to create a new Parameter Class).
 * It also provide you a way to to some additional work after the execution by implementing the returnXXXX method that are call after the execution return the XXXX status.
 * Be aware of the returnProblemCNF method.
 * @author stephane
 *
 */
public abstract class PreProcessorModel extends PreProcessor {
	public static final int DEFAULT_RETURN_VALUE = 0; 
	public static final int RETURN_UNSATISFIABLE = 20;
	public static final int RETURN_SATISFIABLE = 10;
		
	protected int returnDefault = DEFAULT_RETURN_VALUE;
	protected int returnUnSat = RETURN_UNSATISFIABLE;
	protected int returnSat = RETURN_SATISFIABLE;
	protected String description;
	
	public PreProcessorModel(String description, int defaultValue, int unsat, int sat){
		returnDefault = defaultValue;
		returnUnSat = unsat;
		returnSat = sat;
		this.description = description;
	}

	
	@Override
	public abstract String[] getCommandLine(String cnfFile);

	@Override
	public abstract boolean hasTimeout();

	@Override
	public PreProcessorResult runPreProcessor(String[] cmd, String fileOutput) {
		PreProcessorResult res = new PreProcessorResult(); 
		
		BufferedReader input = null;
		BufferedReader inerr = null;
		try{//lance le processus
			res.setBegin(System.currentTimeMillis());
			setRunning(true);
			
			process = Runtime.getRuntime().exec(cmd);

			String line;
			input = new BufferedReader (new InputStreamReader(process.getInputStream()));
			inerr = new BufferedReader (new InputStreamReader(process.getErrorStream()));
			
			while ((line = input.readLine()) != null) 
			{ //verifie les stdin
				//System.out.println(line);
				res.addStdin(line+"\n");
			}
			while ((line = inerr.readLine()) != null) 
			{ //verifie les stderr
				//System.out.println(line);
				res.addStderr(line+"\n");
			}
		}
		catch(IOException e){
			//e.printStackTrace();
			res.setStatus(PreProcessorResultStatus.PROBLEM);
			if(process != null)
				process.destroy();
		}
		finally{
			try{
				if(input != null)
					input.close();
				if(inerr != null)
					inerr.close();
				if(process != null)
					res.setExitVal(process.waitFor());
			}
			catch(Exception e){
				//e.printStackTrace();
				res.setStatus(PreProcessorResultStatus.PROBLEM);
			}
			finally{
				setRunning(false);
			}
		}
		//terminer
		res.setEnd(System.currentTimeMillis());

		//System.out.println("val de retour"+res.getExitVal());
		
		//s'occupe du status
		if(hasBeenStop()) //cas timeout
			res.setStatus(PreProcessorResultStatus.TIMEOUT_REACHED);
		else
			if(res.getStatus() != PreProcessorResultStatus.PROBLEM)
				if(res.getExitVal() == returnUnSat)
				{//UNSAT
					res.setStatus(PreProcessorResultStatus.UNSATISFIABLE) ;
					returnUnSat(res);
				}
				else
					if(res.getExitVal() == returnSat)
					{//SAT
						res.setStatus(PreProcessorResultStatus.SATISFIABLE) ;
						returnUnSat(res);
					}
					else
						if(res.getExitVal() == returnDefault)
						{ //DEFAULT
							res.setStatus(PreProcessorResultStatus.OK) ; 
							returnDefault(res);
						}
						else
						{//PROBLEM					
							res.setStatus(PreProcessorResultStatus.PROBLEM) ;
							returnProblem(res);
						}

		//dernier details
		res.setDescription(description);
		res.setExportPath(fileOutput);
		try{
			if(res.getStatus() == PreProcessorResultStatus.OK)
			{
				res.setCnf(new FileCNF(fileOutput));
				//res.setStat(new Stat(res.getCnf()));
			}
		}
		catch (Exception e) {
			//e.printStackTrace();
			res.setStatus(PreProcessorResultStatus.PROBLEM);
			returnProblemCNF(res);
		}
			
		return res;
	}

	/**
	 * is call when the preprocessor was executed with o problem 
	 * @param res the actual result of the preprocessing
	 */
	protected abstract void returnDefault(PreProcessorResult res);
	/**
	 * is call when the result after the execution of the preprocessor is UNSAT
	 * @param res the actual result of the preprocessing
	 */
	protected abstract void returnUnSat(PreProcessorResult res);
	/**
	 * is call when there was a problem
	 * @param res the actual result of the preprocessing
	 */
	protected abstract void returnProblem(PreProcessorResult res);
	/**
	 * is call when there was a problem creating the result CNF : this operation is done at last, after everything else, it means also that one of the other returnXXX method has been call before.
	 * @param res the actual result of the preprocessing
	 */
	protected abstract void returnProblemCNF(PreProcessorResult res);
	
	/**
	 * is call after the execution of the solver has been stop by the timeout
	 * @param res the actual result of the preprocessing
	 */
	protected abstract void returnHasBeenStop(PreProcessorResult res);

}
